Document Hoster-Stump lower-sum obstruction - #332
Merged
Conversation
…-step Infer Ma-Wang step certificates from recurrence
…erence feat: infer Ma-Wang one-step targets
…nference feat: infer Ma-Wang sequence certificates
feat: infer PF Hadamard weak interlacing
…inference Infer Liu-Wang sequence certificates from recurrences
…dpoint Route zero-to-positive parameter root counts
…currence-inference Tactic: infer product-factor sequence certificates from recurrence
…e-automation-cleanup Infer Product recurrence certificates
…cked-routing Infer affine Favard certificate packets
…fication-inference Infer recurrence identification certificates
Prove adjacent gamma interlacing transfer
Fix Braun--Jal Theorem 4.1 source matrix
Define source-faithful Hoster-Stump interlacing sequences
Add sign-regular matrix predicate API
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Depends on #331.
This audits issue #316 against Hoster--Stump, arXiv:2508.15538, p. 4 and Lemma 2.3(2). The paper's convention that every pair of degree-zero or degree-one polynomials interlaces makes the claimed lower-partial-sum closure false for mixed linear/quadratic sequences.
The PR adds a checked counterexample:
f1 = X + 1f2 = 2 * (X + 3)f3 = (X + 1) * (X + 3)The input satisfies the source-exact sequence predicate: the first pair uses the low-degree convention, and both linear polynomials strictly precede
f3. The final lower sum is(X + 2) * (X + 5), whose roots-2and-5do not bracket the root-1off1.This intentionally does not close #316. A valid replacement needs a stronger pairwise
Prec0hypothesis in addition to elementwise source real-rootedness and nonnegative coefficients.Validation
lake ... build RealRooted.HosterStumpInterlacing